Lambda Calculus --------------- [(Up)](../../README.md#topics) | _See also: [Name Binding](../Name%20Binding/README.md#name-binding), [Logic](../Logic/README.md#logic), [Type Theory](../Type%20Theory/README.md#type-theory), [Functional Programming](../Functional%20Programming/README.md#functional-programming)_ - - - - ### Web resources [functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/110375/is-lambda-calculus-purely-syntactic) ★ [What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/28452/what-are-the-axioms-inference-rules-and-formal-semantics-of-lambda-calculus) ★ [lo.logic - What\'s the point of \$\\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/8259/whats-the-point-of-eta-conversion-in-lambda-calculus) ★ [lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange](https://math.stackexchange.com/questions/802494/whats-the-definition-of-equational-theory-why-is-%CE%BB-logic-free) ★ [lo.logic - Scott on the consistency of the lambda calculus - MathOverflow](https://mathoverflow.net/questions/16752/scott-on-the-consistency-of-the-lambda-calculus) ★ ### Lambda Terms [The largest number representable in 64 bits](https://tromp.github.io/blog/2023/11/24/largest-number) ★ [lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow](https://mathoverflow.net/questions/353514/whatt-the-smallest-lambda-calculus-term-which-is-not-known-to-have-a-normal-for) ★ _(in [Compiler Construction](../Compiler%20Construction/README.md#compiler-construction))_ [Example assembly/machine instruction from lambda calculus](https://stackoverflow.com/questions/67594976/example-assembly-machine-instruction-from-lambda-calculus) ★★ [💭](commentary/Chris%20Pressey.md#example-assembly-machine-instruction-from-lambda-calculus) ### Repositories [maciej-bendkowski/lambda-sampler: Boltzmann sampler utilities for lambda calculus](https://github.com/maciej-bendkowski/lambda-sampler) ★ _(in [Name Binding](../Name%20Binding/README.md#name-binding))_ [mathink/mslambda: Map, Skeleton, Lambda term.](https://github.com/mathink/mslambda) ★ [💭](commentary/Chris%20Pressey.md#mathink-mslambda-map-skeleton-lambda-term) _(in [Name Binding](../Name%20Binding/README.md#name-binding))_ [bacam/sato-maps-agda](https://github.com/bacam/sato-maps-agda) ★ [💭](commentary/Chris%20Pressey.md#bacam-sato-maps-agda) ### Papers [A Short Introduction to the Lambda Calculus](https://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf) ★★ [💭](commentary/Chris%20Pressey.md#a-short-introduction-to-the-lambda-calculus) [Introduction to Lambda Calculus](https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf) ★★ [💭](commentary/Chris%20Pressey.md#introduction-to-lambda-calculus) [Chapter 5: The Untyped Lambda Calculus](https://xiongyingfei.github.io/DPPL/2021/xiong_ch5.pdf) ★★ [Untyped Lambda Calculus](https://www3.cs.stonybrook.edu/~cram/cse526/Spring20/Lectures/untyped-lambda.pdf) ★ [A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure](https://core.ac.uk/reader/47112580) ★ [💭](commentary/Chris%20Pressey.md#a-lambda-calculus-structure-isomorphic-to-gentzen-style-sequent-calculus-structure) The Lambda Calculus is Algebraic (online @ [www.mscs.dal.ca](https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf)) ★★★ [💭](commentary/Chris%20Pressey.md#the-lambda-calculus-is-algebraic) A Lambda Calculus with Naive Substitution (online @ [www.cambridge.org](https://www.cambridge.org/core/journals/journal-of-the-australian-mathematical-society/article/lambda-calculus-with-naive-substitution/2ADB7D36897443688E97F3FEA3A84B64)) [💭](commentary/Chris%20Pressey.md#a-lambda-calculus-with-naive-substitution) [A Graph-like Lambda Calculus for which Leftmost-Outermost Reduction is Optimal](https://link.springer.com/chapter/10.1007/bfb0025740?noAccess=true) ★ [💭](commentary/Chris%20Pressey.md#a-graph-like-lambda-calculus-for-which-leftmost-outermost-reduction-is-optimal) [On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control](https://members.loria.fr/PdeGroote/papers/lpar94.pdf) [💭](commentary/Chris%20Pressey.md#on-the-relation-between-the-λμ-calculus-and-the-syntactic-theory-of-sequential-control) _(in [Computational Complexity](../Computational%20Complexity/README.md#computational-complexity))_ The Typed Lambda Calculus is not Elementary Recursive (online @ [www.cs.cornell.edu](https://www.cs.cornell.edu/courses/cs6110/2012sp/Statman-typed-lambda-calculus.pdf)) ★ _(in [Name Binding](../Name%20Binding/README.md#name-binding))_ [Don’t Substitute Into Abstractions (Functional Pearl)](https://benl.ouroborus.net/papers/2016-dsim/lambda-dsim-20160328.pdf) _(in [Partial Evaluation](../Partial%20Evaluation/README.md#partial-evaluation))_ [A partial evaluator for the untyped lambda-calculus](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/partial-evaluator-for-the-untyped-lambdacalculus/EE324F936F0A009B6766B13FF6755DFC) 🏛️ ### Books The Calculi of Lambda-Conversion (online @ [archive.org](https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941), [archive.org](https://archive.org/details/the-calculi-of-lambda-conversion-couverture-alonzo-church-princeton-university-p)) (borrow with print disabilities @ [archive.org](https://archive.org/details/calculioflambdac0000chur)) 🏛️ Introduction to Combinators and the Lambda Calculus (borrow @ [archive.org](https://archive.org/details/introductiontoco0000hind)) [💭](commentary/Chris%20Pressey.md#introduction-to-combinators-and-the-lambda-calculus)